Celestin Apprentice 5/Apprentice-Release5.iso/Source Code/C/Applications/Moscow ML 1.31/source code/mosml/src/compiler/Elab.sml

Text File | 1996-07-03 | 30.4 KB | 1,029 lines | [TEXT/R*ch]

open List;
open Fnlib Config Mixture Const Smlexc;
open Globals Location Units Asynt Asyntfn Types;

type UEnv = (string * Type) list;   (* Syntax TyVars to TypeVars *)

(* --- Warning printing --- *)

fun isFunType tau =
  case normType tau of
      ARROWt _ => true
    |        _ => false
;

fun unitResultExpected exp tau =
  if isFunType tau then
    (msgIBlock 0;
     errLocation (xLR exp);
     errPrompt "Warning: function-type result is being discarded.";
     msgEOL(); msgEOL();
     msgEBlock())
  else ()
;
(* --- Error printing --- *)

fun typeClash tau1 tau2 =
(
  resetTypePrinter();
  collectExplicitVars tau1;
  collectExplicitVars tau2;
  msgString " of type"; msgEOL();
  errPrompt "  "; printNextType tau1; msgEOL();
  errPrompt "cannot be made to have type"; msgEOL();
  errPrompt "  "; printNextType tau2; msgEOL();
  resetTypePrinter()
);

fun typeClashId (ii : IdInfo) tau1 tau2 =
  let val {qualid, info} = ii in
    msgIBlock 0;
    errLocation (#idLoc info);
    errPrompt "Type clash: identifier "; msgString (showQualId qualid);
    typeClash tau1 tau2;
    msgEBlock();
    raise Toplevel
  end
;

fun unifyId ii tau1 tau2 =
  unify tau1 tau2
  handle Unify => typeClashId ii tau1 tau2
;

fun typeClashPat pat tau1 tau2 =
(
  msgIBlock 0;
  errLocation (xLR pat);
  errPrompt "Type clash: pattern";
  typeClash tau1 tau2;
  msgEBlock();
  raise Toplevel
);

fun unifyPat pat tau1 tau2 =
  unify tau1 tau2
  handle Unify => typeClashPat pat tau1 tau2
;

fun typeClashExp exp tau1 tau2 =
(
  msgIBlock 0;
  errLocation (xLR exp);
  errPrompt "Type clash: expression";
  typeClash tau1 tau2;
  msgEBlock();
  raise Toplevel
);

fun unifyExp exp tau1 tau2 =
  unify tau1 tau2
  handle Unify => typeClashExp exp tau1 tau2
;

fun unifyMatch mrules tau1 tau2 =
  unify tau1 tau2
  handle Unify =>
  let val MRule(pats, exp) = hd mrules in
    msgIBlock 0;
    errLocation (xxLR (hd pats) exp);
    errPrompt "Type clash: match rule";
    typeClash tau1 tau2;
    msgEBlock();
    raise Toplevel
  end
;

fun looksLikeInfixId (ii : IdInfo) =
  case ii of
      {qualid={qual="", ...}, info={withOp=false, ...}} => true
    | _ => false
;

fun isPairPat (_, pat') =
  case pat' of
      RECpat(ref (RECrp(fs, NONE))) => isPairRow fs
    | _ => false
;

fun looksLikeInfixExp (_, exp') =
  case exp' of
    VARexp(ref(RESve{qualid={qual="",...}, info={withOp=false,...}}))
      => true
  | VARexp(ref(OVLve({qualid={qual="",...}, info={withOp=false,...}}, _, _)))
      => true
  | _ => false
;

fun isPairExp (_, exp') =
  case exp' of
    RECexp(ref (RECre fs)) => isPairRow fs
  | _ => false
;

fun newUnknownPair() = type_pair (newUnknown()) (newUnknown());

infix 6 U;

fun list_union [] ys = ys
  | list_union (x :: xs) ys =
      if member x ys then (list_union xs ys) else (x :: list_union xs ys)

fun list_subtract xs [] = xs
  | list_subtract xs ys =
      let fun h [] = []
            | h (x :: xs) = if member x ys then (h xs) else (x :: h xs)
      in h xs end
;

fun xs U ys = list_union xs ys;
fun U_map f = foldR_map list_union f [];

fun unguardedExp (_, exp') =
  case exp' of
    SCONexp _ => []
  | VARexp _ => []
  | RECexp(ref (RECre fields)) =>
      U_map (fn(_, e) => unguardedExp e) fields
  | RECexp(ref (TUPLEre _)) => fatalError "unguardedExp"
  | VECexp es =>
      U_map unguardedExp es
  | LETexp(dec, exp) =>
      unguardedDec dec U unguardedExp exp
  | PARexp exp => unguardedExp exp
  | APPexp(exp1, exp2) =>
      unguardedExp exp1 U unguardedExp exp2
  | INFIXexp _ =>  fatalError "unguardedExp"
  | TYPEDexp(exp, ty) =>
      unguardedExp exp U unguardedTy ty
  | ANDALSOexp(exp1, exp2) =>
      unguardedExp exp1 U unguardedExp exp2
  | ORELSEexp(exp1, exp2) =>
      unguardedExp exp1 U unguardedExp exp2
  | HANDLEexp(exp, mrules) =>
      unguardedExp exp U U_map unguardedMRule mrules
  | RAISEexp exp =>
      unguardedExp exp
  | IFexp(e0, e1, e2) =>
      unguardedExp e0 U unguardedExp e1 U unguardedExp e2
  | FNexp mrules =>
      U_map unguardedMRule mrules
  | WHILEexp(exp1, exp2) =>
      unguardedExp exp1 U unguardedExp exp2
  | SEQexp(exp1, exp2) =>
      unguardedExp exp1 U unguardedExp exp2

and unguardedMRule (MRule(pats, exp)) =
  U_map unguardedPat pats U unguardedExp exp

and unguardedPat (_, pat') =
  case pat' of
    SCONpat _ => []
  | VARpat _ => []
  | WILDCARDpat => []
  | NILpat _ => []
  | CONSpat(_, p) => unguardedPat p
  | EXNILpat _ => []
  | EXCONSpat(_,p) => unguardedPat p
  | EXNAMEpat _ => fatalError "unguardedPat"
  | REFpat p => unguardedPat p
  | RECpat(ref (RECrp(fs, _))) =>
      U_map (fn(_, p) => unguardedPat p) fs
  | RECpat(ref (TUPLErp _)) => fatalError "unguardedPat"
  | VECpat ps =>
      U_map unguardedPat ps
  | INFIXpat _ => fatalError "unguardedPat"
  | PARpat pat => unguardedPat pat
  | TYPEDpat(pat, ty) =>
      unguardedPat pat U unguardedTy ty
  | LAYEREDpat(pat1, pat2) =>
      unguardedPat pat1 U unguardedPat pat2

and unguardedDec (_, dec') =
  case dec' of
    VALdec _ => []
  | PRIM_VALdec _ => []
  | FUNdec _ => fatalError "unguardedDec"
  | TYPEdec tbs => []
  | PRIM_TYPEdec _ => []
  | DATATYPEdec _ => []
  | ABSTYPEdec(_, _, dec2) =>
      unguardedDec dec2
  | EXCEPTIONdec ebs =>
      U_map unguardedExBind ebs
  | LOCALdec (dec1, dec2) =>
      unguardedDec dec1 U unguardedDec dec2
  | OPENdec _ => []
  | EMPTYdec => []
  | SEQdec (dec1, dec2) =>
      unguardedDec dec1 U unguardedDec dec2
  | FIXITYdec _ => []

and unguardedExBind (EXDECexbind(_, SOME ty)) = unguardedTy ty
  | unguardedExBind (EXDECexbind(_, NONE)) = []
  | unguardedExBind (EXEQUALexbind(_,_)) = []

and unguardedValBind (ValBind(pat, exp)) =
  unguardedPat pat U unguardedExp exp

and unguardedValDec (pvbs, rvbs) =
  (U_map unguardedValBind pvbs) U
  (U_map unguardedValBind rvbs)

and unguardedTy (_, ty') =
  case ty' of
    TYVARty ii => [#id(#qualid ii)]
  | RECty fs =>
      U_map (fn(_, ty) => unguardedTy ty) fs
  | CONty(tys, _) =>
      U_map unguardedTy tys
  | FNty(ty1, ty2) =>
      unguardedTy ty1 U unguardedTy ty2
;

nonfix U;

fun scopedTyVars UE unguardedTyVars =
  list_subtract unguardedTyVars (map fst UE)
;

fun incrUE tyvars =
  map (fn tv => (tv, TypeOfTypeVar(newExplicitTypeVar tv))) tyvars
;

fun isExpansiveExp (_, exp') =
  case exp' of
    VARexp _ => false
  | TYPEDexp(exp,_) => isExpansiveExp exp
  | FNexp _ => false
  | _ => true
;

fun expansiveIdsInValBind (ValBind(pat, exp)) acc =
  if (isExpansiveExp exp) then (domPatAcc pat acc) else acc
;

fun closeValBindVE onTop loc (pvbs: ValBind list) VE =
  let val exIds = foldR expansiveIdsInValBind [] pvbs in
    mapEnv (fn id => fn t => generalization onTop loc (member id exIds) t) VE
  end
;

fun lookup_TE (TE : TyEnv) (tycon : IdInfo) =
  let val {qualid, info} = tycon
      val {idLoc, ...} = info
  in
    findInfo tyEnvOfSig TE idLoc qualid
    handle Subscript =>
      errorMsg idLoc ("Unbound type identifier: " ^ showQualId qualid)
  end;

fun lookup_VE (VE : VarEnv) (ii : IdInfo) =
  let val {qualid, info} = ii
      val {idLoc, ...} = info
  in
    specialization(findInfo varEnvOfSig VE idLoc qualid)
    handle Subscript =>
      fatalError "lookup_VE"
  end;

fun lookup_UE (UE : UEnv) loc (ii : IdInfo) =
  let val id = #id(#qualid ii) in
    lookup id UE
    handle Subscript => errorMsg loc ("Unbound type variable: " ^ id)
  end;

fun applyTyCon TE (tycon : IdInfo) ts =
  let val tyname = lookup_TE TE tycon
      val arity = List.length ts
  in
    if #tnArity(!(#info tyname)) <> arity then
      errorMsg (#idLoc (#info tycon))
        ("Arity mismatch: "^showQualId (#qualid tycon))
    else ();
    case #tnStr(!(#info tyname)) of
        NILts =>
          type_con ts tyname
      | TYPEts(pars, body) =>
          type_subst (zip2 pars ts) body
      | DATATYPEts _ =>
          type_con ts tyname
      | REAts _ => fatalError "applyTyCon"
  end;

fun elabTy (UE : UEnv) (TE : TyEnv) (loc, ty') =
  case ty' of
    TYVARty ii =>
      lookup_UE UE loc ii
  | RECty fs =>
      type_rigid_record (map_fields (elabTy UE TE) fs)
  | CONty(ty_list, tycon) =>
      applyTyCon TE tycon (map (elabTy UE TE) ty_list)
  | FNty(ty,ty') =>
      type_arrow (elabTy UE TE ty) (elabTy UE TE ty')
;

fun elabSCon (INTscon i)    = type_int
  | elabSCon (CHARscon c)   = type_char
  | elabSCon (REALscon r)   = type_real
  | elabSCon (STRINGscon s) = type_string
;

fun elabPat (UE : UEnv) (VE : VarEnv) (TE : TyEnv)
                (pat as (_, pat')) (pat_t : Type) (PE : VarEnv) =
  case pat' of
    SCONpat scon =>
      (unifyPat pat (elabSCon scon) pat_t; PE)
  | VARpat ii =>
      bindInEnv PE (#id (#qualid ii)) (trivial_scheme pat_t)
  | WILDCARDpat => PE
  | NILpat ii => (unifyPat pat (lookup_VE VE ii) pat_t; PE)
  | CONSpat(ii, p) =>
      let val id_t = lookup_VE VE ii
          val p_t = newUnknown()
          val res_t = newUnknown()
      in
        unifyId ii id_t (type_arrow p_t res_t);
        if (looksLikeInfixId ii) andalso (isPairPat p) then
          (unify p_t (newUnknownPair())
           handle Unify =>
             typeClashId ii id_t (type_arrow (newUnknownPair()) res_t))
        else ();
        unifyPat pat res_t pat_t;
        elabPat UE VE TE p p_t PE
      end
  | EXNILpat ii =>
      let val id_t = lookup_VE VE ii in
        unifyId ii id_t type_exn;
        unifyPat pat type_exn pat_t;
        PE
      end
  | EXCONSpat(ii, p) =>
      let val id_t = lookup_VE VE ii
          val p_t = newUnknown()
      in
        unifyId ii id_t (type_arrow p_t type_exn);
        if looksLikeInfixId ii andalso isPairPat p then
          (unify p_t (newUnknownPair())
           handle Unify =>
             typeClashId ii id_t (type_arrow (newUnknownPair()) type_exn))
        else ();
        unifyPat pat type_exn pat_t;
        elabPat UE VE TE p p_t PE
      end
  | EXNAMEpat _ => fatalError "elabPat"
  | REFpat p =>
      let val p_t = newUnknown() in
        unifyPat pat (type_ref p_t) pat_t;
        elabPat UE VE TE p p_t PE
      end
  | RECpat(ref (RECrp(fs, dots))) =>
      let val ls = map fst fs
          val ps = map snd fs
          val ts = map (fn _ => newUnknown()) ps
          val fs_t = zip2 ls ts
          fun reportClash isRigid =
            let val ts' = map (fn _ => newUnknown()) ps
                val fs_t' = zip2 ls ts'
            in
              if isRigid then
                typeClashPat pat (type_rigid_record fs_t') pat_t
              else
                typeClashPat pat
                  (type_flexible_record fs_t' (fresh3DotType())) pat_t
            end
      in
        (case dots of
            NONE =>     (unify (type_rigid_record fs_t) pat_t
                         handle Unify => reportClash true)
          | SOME rho => (unify (type_flexible_record fs_t rho) pat_t
                         handle Unify => reportClash false));
        foldL_zip (elabPat UE VE TE) PE ps ts
      end
  | RECpat(ref (TUPLErp _)) => fatalError "elabPat"
  | VECpat ps =>
      let val p_t = newUnknown() in
        unifyPat pat (type_vector p_t) pat_t;
        foldL (fn p => fn PE => elabPat UE VE TE p p_t PE) PE ps
      end
  | PARpat p =>
      elabPat UE VE TE p pat_t PE
  | INFIXpat _ => fatalError "elabPat"
  | TYPEDpat(p,ty) =>
      let val ty_t = elabTy UE TE ty
          val PE' = elabPat UE VE TE p pat_t PE
      in
        unifyPat p pat_t ty_t;
        PE'
      end
  | LAYEREDpat(p1,p2) =>
      elabPat UE VE TE p2 pat_t
        (elabPat UE VE TE p1 pat_t PE)
;

fun freshTyName tycon arity =
  { qualid=mkGlobalName tycon,
    info=ref { tnStamp=newTypeStamp(), tnArity=arity,
               tnEqu=TRUEequ, tnStr=NILts }}
;

fun makeTyName tyvar_list tycon =
  let val arity = List.length tyvar_list
  in freshTyName tycon arity end
;

fun initialDatBindTE (dbs : DatBind list)=
  foldL
    (fn (tyvar_list, tycon, _) => fn env =>
       let val id = #id (#qualid tycon)
       in bindInEnv env id (makeTyName tyvar_list id) end)
    NILenv dbs
;

fun absTE (TE : TyEnv) =
  traverseEnv
    (fn id => fn tyname =>
       let val {info, ...} = tyname in
         case #tnStr(!info) of
             DATATYPEts dt =>
               (setTnEqu info FALSEequ;
                setConstructors (!currentSig) dt [])
           | _ => fatalError "absTE"
       end)
    TE
;

fun elabTypBind (TE : TyEnv) ((tyvars, tycon, ty) : TypBind) =
  let val id = #id(#qualid tycon)
      val pars = map (fn tyvar => #id(#qualid tyvar)) tyvars
      val vs = map (fn tv => newExplicitTypeVar tv) pars
      val us = map TypeOfTypeVar vs
      val UE = zip2 pars us
      val t = elabTy UE TE ty
      val tyname = makeTyName tyvars id
  in
    setTnStr (#info tyname) (TYPEts(vs, t));
    (id, tyname)
  end
;

fun elabTypBindList (TE : TyEnv) (tbs : TypBind list) =
  foldL_map (fn (id, tyname) => fn env => bindInEnv env id tyname)
            (elabTypBind TE) NILenv tbs
;

fun elabTypBindList_opt (TE : TyEnv) = fn
    SOME tbs => elabTypBindList TE tbs
  | NONE => NILenv
;

fun elabPrimTypBind equ ((tyvars, tycon) : TypDesc) =
  let val id = #id(#qualid tycon)
      val tyname = makeTyName tyvars id
  in
    setTnEqu (#info tyname) equ;
    (id, tyname)
  end;

fun elabPrimTypBindList equ (tbs : TypDesc list) =
  foldL_map (fn (id, tyname) => fn env => bindInEnv env id tyname)
            (elabPrimTypBind equ) NILenv tbs
;

fun closeEE EE =
  mapEnv (fn excon => fn t => generalization false nilLocation true t) EE
;

fun openVE VE =
  mapEnv (fn id => fn sch => TypeOfScheme sch) VE
;

fun isRecTy (loc, ty') =
  case ty' of
    RECty [] => false
  | RECty _ => true
  | _ => false
;

fun arityOfRecTy (loc, ty') =
  case ty' of
      RECty fs => List.length fs
    | _ => fatalError "arityOfRecTy"
;

fun elabConBind (UE : UEnv) (TE : TyEnv) res_t = fn
    ConBind(ii, SOME ty) =>
      let val ci = getConInfo ii
          val arg_t = (elabTy UE TE ty)
      in
        setConType ci
          (generalization false nilLocation false (type_arrow arg_t res_t));
        if #conSpan(!ci) <> 1 andalso isRecTy ty then
          (setConArity ci (arityOfRecTy ty);
           setConIsGreedy ci true)
        else ();
        { qualid= #qualid(!(#idKind(#info ii))), info=ci }
      end
  | ConBind(ii, NONE) =>
      let val ci = getConInfo ii in
        setConType ci (generalization false nilLocation false res_t);
        { qualid= #qualid(!(#idKind(#info ii))), info=ci }
      end
;

fun setEquality (TE :TyEnv) =
  traverseEnv
    (fn _ => fn tyname =>
       let val {info, ...} = tyname in
         case #tnStr(!info) of
             NILts => fatalError "setEquality"
           | TYPEts(_, t) =>
               setTnEqu info
                 (if typeViolatesEquality t then FALSEequ else TRUEequ)
           | DATATYPEts _ => fatalError "setEquality"
           | REAts _ => fatalError "setEquality"
       end)
    TE
;

val equAttrReset = ref false;

fun maximizeEquality (TE : TyEnv) =
(
  equAttrReset := true;
  while !equAttrReset do
    (equAttrReset := false;
     traverseEnv
       (fn _ => fn tyname =>
         let val {info, ...} = tyname in
           case #tnStr(!info) of
               NILts => fatalError "maximizeEquality"
             | TYPEts _ => fatalError "maximizeEquality"
             | DATATYPEts dt =>
                 (let val CE = findConstructors (!currentSig) dt in
                    case #tnEqu(!info) of
                        FALSEequ => ()
                      | TRUEequ  =>
                          if exists (fn ci => schemeViolatesEquality
                                       (#conType (!(#info ci))))
                                    CE
                          then
                            (setTnEqu info FALSEequ; equAttrReset := true)
                          else ()
                      | REFequ  => fatalError "maximizeEquality"
                  end)
             | REAts _ => fatalError "maximizeEquality"
         end)
       TE)
);

fun setTags (cbs : ConBind list) =
  let val span = List.length cbs
      fun loop n = fn
          [] => ()
        | (ConBind(ii, _)) :: rest =>
            let val {info={idLoc, ...}, ...} = ii
                val () =
                  if n > maxBlockTag then
                    errorMsg idLoc
     ("Implementation restriction: datatype cannot declare more than "^
      makestring(maxBlockTag + 1) ^" constructors.")
                  else ();
                val ci = getConInfo ii
            in
              setConTag ci n;
              setConSpan ci span;
              loop (n+1) rest
            end
  in loop 0 cbs end
;

fun VEofCE (CE : ConEnv) =
  foldR (fn cs => fn env =>
           let val {qualid, info} = cs
           in bindInEnv env (#id qualid) (#conType (!info)) end)
        NILenv CE
;

fun cons x xs = x :: xs;

fun elabDatBind (TE:TyEnv) ((tyvars, tycon, conbind_list) : DatBind) =
  let val pars = map (fn ii => #id(#qualid ii)) tyvars
      val () = setTags conbind_list
      val () = incrBindingLevel()
      val vs = map (fn tv => newExplicitTypeVar tv) pars
      val () = decrBindingLevel()
      val us = map TypeOfTypeVar vs
      val UE = zip2 pars us
      val tyname = lookup_TE TE tycon
      val t = type_con us tyname
      val CE = foldL_map cons (elabConBind UE TE t) [] conbind_list
  in
    setTnStr (#info tyname) (DATATYPEts (registerConstructors(rev CE)));
    VEofCE CE
  end
;

fun elabDatBindList (TE : TyEnv) (dbs : DatBind list) =
  foldL_map (fn env' => fn env => plusEnv env env')
            (elabDatBind TE) NILenv dbs
;

fun elabExBind (UE : UEnv) (VE : VarEnv) (TE : TyEnv) = fn
    EXDECexbind(ii, SOME ty) =>
      let val ei = getExConInfo ii
          val arg_t = (elabTy UE TE ty)
      in
        if typeIsImperative arg_t then ()
        else errorMsg (xLR ty) "Non-imperative exception type";
        if isExConStatic ei andalso isRecTy ty then
          (setExConArity ei (arityOfRecTy ty);
           setExConIsGreedy ei true)
        else ();
        (#id(#qualid ii), type_arrow arg_t type_exn)
      end
  | EXDECexbind(ii, NONE) =>
      (#id(#qualid ii), type_exn)
  | EXEQUALexbind(ii, ii') =>
      (#id(#qualid ii), lookup_VE VE ii')
;

fun elabExBindList (UE : UEnv) (VE : VarEnv) (TE : TyEnv) ebs =
  closeEE (foldL_map (fn (id, tau) => fn env => bindInEnv env id tau)
                     (elabExBind UE VE TE) NILenv ebs)
;

(* OVL1TXXo is not a true overloaded type, *)
(* because it needn't be resolved to `int', `real', or `string'. *)
(* This is only a hack to catch the type inferred by the *)
(* type-checker... Thus the attribute `overloaded' mustn't be *)
(* turned on in the type variable. *)
(* The same is true of OVL1TPUo. *)

fun elabOvlExp t ovltype =
  case ovltype of
      REGULARo =>
        fatalError "elabOvlExp"
    | OVL1NNo =>
        (setCurrentBindingLevel true t;
         type_arrow t t)
    | OVL1NSo =>
        (setCurrentBindingLevel true t;
         type_arrow t type_string)
    | OVL2NNBo =>
        (setCurrentBindingLevel true t;
         type_arrow (type_pair t t) type_bool)
    | OVL2NNNo =>
        (setCurrentBindingLevel true t;
         type_arrow (type_pair t t) t)
    | OVL1TXXo =>
        (setCurrentBindingLevel false t;
         type_arrow t t)
    | OVL1TPUo =>
        (setCurrentBindingLevel false t;
         type_arrow
           (type_arrow type_ppstream (type_arrow t type_unit))
           type_unit)
;

fun elabExp (UE : UEnv) (VE : VarEnv) (TE : TyEnv)
                 (exp as (_, exp')) exp_t =
  case exp' of
    SCONexp scon =>
      unifyExp exp (elabSCon scon) exp_t
  | VARexp(ref (RESve ii)) =>
      unifyExp exp (lookup_VE VE ii) exp_t
  | VARexp(ref (OVLve(_, ovltype, tau))) =>
      unifyExp exp (elabOvlExp tau ovltype) exp_t
  | FNexp mrules =>
      elabMatch UE VE TE mrules exp_t
  | APPexp(func, arg) =>
      let val func_t = newUnknown()
          val () = elabExp UE VE TE func func_t
          val arg_t = newUnknown()
          val res_t = newUnknown()
      in
        unifyExp func func_t (type_arrow arg_t res_t);
        if looksLikeInfixExp func andalso isPairExp arg then
          (unify arg_t (newUnknownPair())
           handle Unify =>
             typeClashExp func func_t (type_arrow (newUnknownPair()) res_t))
        else ();
        unifyExp exp res_t exp_t;
        elabExp UE VE TE arg arg_t
      end
  | LETexp(dec, body) =>
      let val (VE', TE') = elabDec UE VE TE false dec
      in elabExp UE (plusEnv VE VE') (plusEnv TE TE') body exp_t end
  | RECexp(ref (RECre fs)) =>
      let val ls = map fst fs
          val es = map snd fs
          val ts = map (fn _ => newUnknown()) es
          val fs_t = zip2 ls ts
      in
        (unify (type_rigid_record fs_t) exp_t
         handle Unify =>
           let val ts' = map (fn _ => newUnknown()) es
               val fs_t' = zip2 ls ts'
           in typeClashExp exp (type_rigid_record fs_t') exp_t end);
        app2 (elabExp UE VE TE) es ts
      end
  | RECexp(ref (TUPLEre _)) => fatalError "elabExp"
  | VECexp es =>
      let val e_t = newUnknown() in
        app (fn e => elabExp UE VE TE e e_t) es;
        unifyExp exp (type_vector e_t) exp_t
      end
  | PARexp e =>
      elabExp UE VE TE e exp_t
  | INFIXexp _ => fatalError "elabExp: unresolved infix exp"
  | TYPEDexp(e,ty) =>
      let val ty_t = elabTy UE TE ty in
        elabExp UE VE TE e exp_t;
        unifyExp e exp_t ty_t
      end
  | ANDALSOexp(e1, e2) =>
      (elabExp UE VE TE e1 type_bool;
       elabExp UE VE TE e2 type_bool;
       unifyExp exp type_bool exp_t)
  | ORELSEexp(e1, e2) =>
      (elabExp UE VE TE e1 type_bool;
       elabExp UE VE TE e2 type_bool;
       unifyExp exp type_bool exp_t)
  | HANDLEexp(e, mrules) =>
      (elabExp UE VE TE e exp_t;
       elabMatch UE VE TE mrules (type_arrow type_exn exp_t))
  | RAISEexp e =>
      elabExp UE VE TE e type_exn
  | IFexp(e0, e1, e2) =>
      (elabExp UE VE TE e0 type_bool;
       elabExp UE VE TE e1 exp_t;
       elabExp UE VE TE e2 exp_t)
  | WHILEexp(e1, e2) =>
      let val e2_t = newUnknown() in
        elabExp UE VE TE e1 type_bool;
        elabExp UE VE TE e2 e2_t;
        unitResultExpected e2 e2_t;
        unifyExp exp type_unit exp_t
      end
  | SEQexp(e1, e2) =>
      let val e1_t = newUnknown() in
        elabExp UE VE TE e1 e1_t;
        unitResultExpected e1 e1_t;
        elabExp UE VE TE e2 exp_t
      end

and elabExpSeq UE VE TE es ts =
  let fun loop [] [] = ()
        | loop (e :: es) (t :: ts) =
            (elabExp UE VE TE e t; loop es ts)
        | loop _ _ = fatalError "elabExpSeq"
  in loop es ts end

and elabMatch UE VE TE mrules match_t =
  let val MRule(pats1,_) = hd mrules
      val arg_ts = map (fn pat => newUnknown()) pats1
      val res_t = newUnknown()
  in
    unifyMatch mrules (foldR type_arrow res_t arg_ts) match_t;
    app (fn MRule(pats, exp) => elabMRule UE VE TE exp res_t pats arg_ts)
            mrules
  end

and elabMRule UE VE TE exp res_t pats arg_ts =
  case (pats, arg_ts) of
      ([], []) => elabExp UE VE TE exp res_t
    | (pat :: pats', arg_t :: arg_ts') =>
        let val VE' = elabPat UE VE TE pat arg_t VE
        in elabMRule UE VE' TE exp res_t pats' arg_ts' end
    | (_, _) => fatalError "elabMRule"

and elabDec (UE : UEnv) (VE : VarEnv) (TE : TyEnv)
            (onTop : bool) (loc, dec') =
  case dec' of
    VALdec (pvbs, rvbs) =>
      let val tyvars = scopedTyVars UE (unguardedValDec (pvbs, rvbs))
          val ()   = incrBindingLevel()
          val UE'  = (incrUE tyvars) @ UE
          val VE'  = elabValBind UE' VE TE pvbs
          val VE'' = elabRecValBind UE' VE TE rvbs
      in
        decrBindingLevel();
        (closeValBindVE onTop loc pvbs (plusEnv VE' VE''), NILenv)
      end
  | PRIM_VALdec pbs =>
      let val VE' = foldL_map (fn(id, sc) => fn acc => bindInEnv acc id sc)
                              (elabPrimValBind TE)
                              NILenv pbs
      in (VE', NILenv) end
  | FUNdec _ => fatalError "elabDec"
  | TYPEdec tbs =>
      let val tbsTE = elabTypBindList TE tbs in
        setEquality tbsTE;
        (NILenv, tbsTE)
      end
  | PRIM_TYPEdec(equ, tbs) =>
      (NILenv, elabPrimTypBindList equ tbs)
  | DATATYPEdec(dbs, tbs_opt) =>
      let val dbsTE = initialDatBindTE dbs
          val tbsTE = elabTypBindList_opt (plusEnv TE dbsTE) tbs_opt
          (* Here dbsTE will get destructively updated too. *)
          val CE = elabDatBindList (plusEnv (plusEnv TE dbsTE) tbsTE) dbs
      in
        maximizeEquality dbsTE;
        setEquality tbsTE;
        (CE, plusEnv dbsTE tbsTE)
      end
  | ABSTYPEdec(dbs, tbs_opt, dec2) =>
      let val dbsTE = initialDatBindTE dbs
          val tbsTE = elabTypBindList_opt (plusEnv TE dbsTE) tbs_opt
          (* Here dbsTE will get destructively updated too. *)
          val CE = elabDatBindList (plusEnv (plusEnv TE dbsTE) tbsTE) dbs
          val () = maximizeEquality dbsTE
          val () = setEquality tbsTE
          val (VE2, TE2) =
            elabDec UE (plusEnv VE CE)
                    (plusEnv (plusEnv TE dbsTE) tbsTE) onTop dec2
      in
        (* Now let's destructively update the equality attributes *)
        (* and the lists of constructors! *)
        (* Here VE2 and TE2 will be implicitly influenced too. *)
        absTE dbsTE;
        setEquality tbsTE;
        (VE2, plusEnv(plusEnv dbsTE tbsTE) TE2)
      end
  | EXCEPTIONdec ebs =>
      (elabExBindList UE VE TE ebs, NILenv)
  | LOCALdec (dec1, dec2) =>
      let val (VE', TE')  = elabDec UE VE TE false dec1
          val (VE'',TE'') =
            elabDec UE (plusEnv VE VE') (plusEnv TE TE') onTop dec2
      in (VE'', TE'') end
  | OPENdec ids =>
      let val VE' =
            foldL (fn id => fn acc =>
                     bindTopInEnv acc (#uVarEnv (findSig loc id)))
                  NILenv ids
              val TE' =
            foldL (fn id => fn acc =>
                     bindTopInEnv acc (#uTyEnv (findSig loc id)))
                  NILenv ids
      in (VE', TE') end
  | EMPTYdec => (NILenv, NILenv)
  | SEQdec (dec1, dec2) =>
      let val (VE', TE')  =
            elabDec UE VE TE onTop dec1
          val (VE'',TE'') =
            elabDec UE (plusEnv VE VE') (plusEnv TE TE') onTop dec2
      in (plusEnv VE' VE'', plusEnv TE' TE'') end
  | FIXITYdec _ => (NILenv, NILenv)

and elabValBind (UE : UEnv) (VE : VarEnv) (TE : TyEnv)
                (vbs : ValBind list) =
  let val ps = map (fn ValBind(p,e) => p) vbs
      val es = map (fn ValBind(p,e) => e) vbs
      val pts = map (fn _ => newUnknown()) ps
      val VE' = foldL_zip (elabPat UE VE TE) NILenv ps pts
  in
    app2 (elabExp UE VE TE) es pts;
    openVE VE'
  end

and elabRecValBind (UE : UEnv) (VE : VarEnv) (TE : TyEnv)
                   (vbs : ValBind list) =
  let val ps = map (fn ValBind(p,e) => p) vbs
      val es = map (fn ValBind(p,e) => e) vbs
      val pts = map (fn _ => newUnknown()) ps
      val VE' = foldL_zip (elabPat UE VE TE) NILenv ps pts
      val rec_VE = plusEnv VE VE'
  in
    app2 (elabExp UE rec_VE TE) es pts;
    openVE VE'
  end

and elabPrimValBind TE (ii, ty, _, _) =
  let val tyvars = varsOfTy ty
      val pars = map (fn tyvar => #id(#qualid tyvar)) tyvars
      val vs = map (fn tv => newExplicitTypeVar tv) pars
      val us = map TypeOfTypeVar vs
      val UE = zip2 pars us
      val ty_t = elabTy UE TE ty
  in (#id(#qualid ii), mkScheme vs ty_t) end
;

fun elabToplevelDec (dec : Dec) =
(
  if unguardedDec dec <> [] then
    errorMsg (xLR dec) "Unguarded type variables at the top-level"
  else ();
  resetBindingLevel();
  elabDec [] (mkGlobalVE()) (mkGlobalTE()) true dec
);


(* --- Signatures --- *)

fun unguardedExDesc (_, SOME ty) = unguardedTy ty
  | unguardedExDesc (_, NONE) = []
;

fun elabValDesc (TE : TyEnv) ((ii, ty) : ValDesc) =
  let val tyvars = varsOfTy ty
      val pars = map (fn tyvar => #id(#qualid tyvar)) tyvars
      val vs = map (fn tv => newExplicitTypeVar tv) pars
      val us = map TypeOfTypeVar vs
      val UE = zip2 pars us
      val ty_t = elabTy UE TE ty
  in (#id(#qualid ii), mkScheme vs ty_t) end
;

fun elabExDesc (UE : UEnv) (VE : VarEnv) (TE : TyEnv)
               ((ii, ty_opt) : ExDesc) =
  let val {qualid={id, ...}, ...} = ii
  in
    case ty_opt of
      SOME ty =>
        let val ei = getExConInfo ii
            val arg_t = (elabTy UE TE ty)
        in
          if typeIsImperative arg_t then ()
          else errorMsg (xLR ty) "Non-imperative exception type";
          if isExConStatic ei andalso isRecTy ty then
            (setExConArity ei (arityOfRecTy ty);
             setExConIsGreedy ei true)
          else ();
          (id, type_arrow arg_t type_exn)
        end
    | NONE =>
        (id, type_exn)
  end;

fun elabExDescList (UE : UEnv) (VE : VarEnv) (TE : TyEnv) eds =
  closeEE (foldL_map (fn (id, tau) => fn env => bindInEnv env id tau)
                     (elabExDesc UE VE TE) NILenv eds)
;

fun elabSpec (VE : VarEnv) (TE : TyEnv) (loc, spec') =
  case spec' of
    VALspec vds =>
      let val VE' = foldL_map (fn(id, sc) => fn acc => bindInEnv acc id sc)
                              (elabValDesc TE)
                              NILenv vds
      in (VE', NILenv) end
  | PRIM_VALspec pvs =>
      let val VE' = foldL_map (fn(id, sc) => fn acc => bindInEnv acc id sc)
                              (elabPrimValBind TE)
                              NILenv pvs
      in (VE', NILenv) end
  | TYPEDESCspec(equ, tds) =>
      (NILenv, elabPrimTypBindList equ tds)
  | TYPEspec tbs =>
      let val tbsTE = elabTypBindList TE tbs in
        setEquality tbsTE;
        (NILenv, tbsTE)
      end
  | DATATYPEspec(dbs, tbs_opt) =>
      let val dbsTE = initialDatBindTE dbs
          val tbsTE = elabTypBindList_opt (plusEnv TE dbsTE) tbs_opt
          (* Here dbsTE will get destructively updated too. *)
          val CE = elabDatBindList (plusEnv (plusEnv TE dbsTE) tbsTE) dbs
      in
        maximizeEquality dbsTE;
        setEquality tbsTE;
        (CE, plusEnv dbsTE tbsTE)
      end
  | EXCEPTIONspec eds =>
      (if U_map unguardedExDesc eds <> [] then
         errorMsg loc "Type variables in an exception description"
       else ();
       (elabExDescList [] VE TE eds, NILenv))
  | LOCALspec (spec1, spec2) =>
      let val (VE', TE')  = elabSpec VE TE spec1
          val (VE'',TE'') =
            elabSpec (plusEnv VE VE') (plusEnv TE TE') spec2
      in (VE'', TE'') end
  | OPENspec ids =>
      let val VE' =
            foldL (fn id => fn acc =>
                     bindTopInEnv acc (#uVarEnv (findSig loc id)))
                  NILenv ids
              val TE' =
            foldL (fn id => fn acc =>
                     bindTopInEnv acc (#uTyEnv (findSig loc id)))
                  NILenv ids
      in (VE', TE') end
  | EMPTYspec => (NILenv, NILenv)
  | SEQspec (spec1, spec2) =>
      let val (VE', TE')  = elabSpec VE TE spec1
          val (VE'',TE'') =
            elabSpec (plusEnv VE VE') (plusEnv TE TE') spec2
      in (plusEnv VE' VE'', plusEnv TE' TE'') end
;

fun elabToplevelSpec (spec : Spec) =
(
  resetBindingLevel();
  elabSpec (mkGlobalVE()) (mkGlobalTE()) spec
);